Inference at * 1 0 
Iof proof for Lemma eq atom eq false elim:



1. x : Atom
2. y : Atom
3. x =a y = ff
  (x = y) 

latex

 by PERMUTE{1:n, 2:n, 3:n, 4:n, 2:n, 5:n, 3:n, 4:n, 6:n, 7:n, 8:n, 9:n, 10:n} 

latex

 1: .....wf..... NILNIL

 1:   (x =a y = ff)  
 2: .....wf..... NILNIL

 2:   ((x =a y))  
 3: .....wf..... NILNIL

 3:   ((x = y))  
 4: .....wf..... NILNIL

 4:   x =a y  
 5: .....wf..... NILNIL

 5:   ((x =a y))  
 6: .....wf..... NILNIL

 6:   (x =a y)  
 7: .....wf..... NILNIL

 7:   (x = y)  
 8: .....wf..... NILNIL

 8:   x  Atom
 9: .....wf..... NILNIL

 9:   y  Atom
 10: 

 10: 3. (x = y)
 10:   (x = y)
 .

Definitions	t  T, x:A  B(x), P  Q, b, b, f(a), x:AB(x), , A, ff, x =a y, , s = t, Atom, P & Q, x:A. B(x), P  Q, P  Q
Lemmas	assert of eq atom, not functionality wrt iff, assert of bnot, eqff to assert, iff transitivity